$\forall$${\it ds}$:$z$:Id fp$\rightarrow$ Type. timedState(${\it ds}$) $\in$ Type